Deducibility Constraints, Equational Theory and Electronic Money
Identifieur interne : 004C78 ( Main/Exploration ); précédent : 004C77; suivant : 004C79Deducibility Constraints, Equational Theory and Electronic Money
Auteurs : Sergiu Bursuc [France] ; Hubert Comon-Lundh [France] ; Stéphanie Delaune [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: The starting point of this work is a case study (from France Télécom) of an electronic purse protocol. The goal was to prove that the protocol is secure or that there is an attack. Modeling the protocol requires algebraic properties of a fragment of arithmetic, typically containing modular exponentiation. The usual equational theories described in papers on security protocols are too weak: the protocol cannot even be executed in these models. We consider here an equational theory which is powerful enough for the protocol to be executed, and for which unification is still decidable. Our main result is the decidability of the so-called intruder deduction problem, i.e. security in presence of a passive attacker, taking the algebraic properties into account. Our equational theory is a combination of several equational theories over non-disjoint signatures.
Url:
DOI: 10.1007/978-3-540-73147-4_10
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003C81
- to stream Istex, to step Curation: 003C37
- to stream Istex, to step Checkpoint: 001063
- to stream Main, to step Merge: 004E12
- to stream Main, to step Curation: 004C78
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Deducibility Constraints, Equational Theory and Electronic Money</title><author><name sortKey="Bursuc, Sergiu" sort="Bursuc, Sergiu" uniqKey="Bursuc S" first="Sergiu" last="Bursuc">Sergiu Bursuc</name></author><author><name sortKey="Comon Lundh, Hubert" sort="Comon Lundh, Hubert" uniqKey="Comon Lundh H" first="Hubert" last="Comon-Lundh">Hubert Comon-Lundh</name></author><author><name sortKey="Delaune, Stephanie" sort="Delaune, Stephanie" uniqKey="Delaune S" first="Stéphanie" last="Delaune">Stéphanie Delaune</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FD699B7C6B695FEA5C2410E8BC561F0FE0F1DDA6</idno><date when="2007" year="2007">2007</date><idno type="doi">10.1007/978-3-540-73147-4_10</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-BZ3XJN85-V/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003C81</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003C81</idno><idno type="wicri:Area/Istex/Curation">003C37</idno><idno type="wicri:Area/Istex/Checkpoint">001063</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001063</idno><idno type="wicri:doubleKey">0302-9743:2007:Bursuc S:deducibility:constraints:equational</idno><idno type="wicri:Area/Main/Merge">004E12</idno><idno type="wicri:Area/Main/Curation">004C78</idno><idno type="wicri:Area/Main/Exploration">004C78</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Deducibility Constraints, Equational Theory and Electronic Money</title><author><name sortKey="Bursuc, Sergiu" sort="Bursuc, Sergiu" uniqKey="Bursuc S" first="Sergiu" last="Bursuc">Sergiu Bursuc</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>Laboratoire Spécification & Vérification, ENS de Cachan & CNRS UMR 8643</wicri:regionArea><wicri:noRegion>ENS de Cachan & CNRS UMR 8643</wicri:noRegion><wicri:noRegion>ENS de Cachan & CNRS UMR 8643</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Comon Lundh, Hubert" sort="Comon Lundh, Hubert" uniqKey="Comon Lundh H" first="Hubert" last="Comon-Lundh">Hubert Comon-Lundh</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>Laboratoire Spécification & Vérification, ENS de Cachan & CNRS UMR 8643</wicri:regionArea><wicri:noRegion>ENS de Cachan & CNRS UMR 8643</wicri:noRegion><wicri:noRegion>ENS de Cachan & CNRS UMR 8643</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Delaune, Stephanie" sort="Delaune, Stephanie" uniqKey="Delaune S" first="Stéphanie" last="Delaune">Stéphanie Delaune</name><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The starting point of this work is a case study (from France Télécom) of an electronic purse protocol. The goal was to prove that the protocol is secure or that there is an attack. Modeling the protocol requires algebraic properties of a fragment of arithmetic, typically containing modular exponentiation. The usual equational theories described in papers on security protocols are too weak: the protocol cannot even be executed in these models. We consider here an equational theory which is powerful enough for the protocol to be executed, and for which unification is still decidable. Our main result is the decidability of the so-called intruder deduction problem, i.e. security in presence of a passive attacker, taking the algebraic properties into account. Our equational theory is a combination of several equational theories over non-disjoint signatures.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Bursuc, Sergiu" sort="Bursuc, Sergiu" uniqKey="Bursuc S" first="Sergiu" last="Bursuc">Sergiu Bursuc</name></noRegion><name sortKey="Bursuc, Sergiu" sort="Bursuc, Sergiu" uniqKey="Bursuc S" first="Sergiu" last="Bursuc">Sergiu Bursuc</name><name sortKey="Comon Lundh, Hubert" sort="Comon Lundh, Hubert" uniqKey="Comon Lundh H" first="Hubert" last="Comon-Lundh">Hubert Comon-Lundh</name><name sortKey="Comon Lundh, Hubert" sort="Comon Lundh, Hubert" uniqKey="Comon Lundh H" first="Hubert" last="Comon-Lundh">Hubert Comon-Lundh</name><name sortKey="Delaune, Stephanie" sort="Delaune, Stephanie" uniqKey="Delaune S" first="Stéphanie" last="Delaune">Stéphanie Delaune</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004C78 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004C78 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:FD699B7C6B695FEA5C2410E8BC561F0FE0F1DDA6
|texte= Deducibility Constraints, Equational Theory and Electronic Money
}}
| This area was generated with Dilib version V0.6.33. |  |